Left Termination of the query pattern
mergesort(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 189 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 275 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 23 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇒, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇒, 15 ms)
        ↳25 QDP
        ↳26 Rewriting (⇔, 199 ms)
        ↳27 QDP
        ↳28 Rewriting (⇔, 0 ms)
        ↳29 QDP
        ↳30 QDPQMonotonicMRRProof (⇔, 1416 ms)
        ↳31 QDP
        ↳32 DependencyGraphProof (⇔, 0 ms)
        ↳33 TRUE
    ↳34 PiDP
        ↳35 UsableRulesProof (⇔, 0 ms)
        ↳36 PiDP
        ↳37 PiDPToQDPProof (⇒, 0 ms)
        ↳38 QDP
        ↳39 Rewriting (⇔, 0 ms)
        ↳40 QDP
        ↳41 UsableRulesProof (⇔, 0 ms)
        ↳42 QDP
        ↳43 QReductionProof (⇔, 0 ms)
        ↳44 QDP
        ↳45 QDPOrderProof (⇔, 0 ms)
        ↳46 QDP
        ↳47 DependencyGraphProof (⇔, 0 ms)
        ↳48 TRUE

(0) Obligation:

Clauses:

mergesort([], []).
mergesort(.(X, []), .(X, [])).
mergesort(.(X, .(Y, Xs)), Ys) :- ','(split(.(X, .(Y, Xs)), X1s, X2s), ','(mergesort(X1s, Y1s), ','(mergesort(X2s, Y2s), merge(Y1s, Y2s, Ys)))).
split([], [], []).
split(.(X, Xs), .(X, Ys), Zs) :- split(Xs, Zs, Ys).
merge([], Xs, Xs).
merge(Xs, [], Xs).
merge(.(X, Xs), .(Y, Ys), .(X, Zs)) :- ','(=(X, Y), merge(.(X, Xs), Ys, Zs)).

Query: mergesort(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

splitA(.(X1, X2), .(X1, X3), X4) :- splitA(X2, X4, X3).
splitD(X1, X2, .(X1, X3), X4) :- splitA(X2, X4, X3).
mergesortE(.(X1, .(X2, X3)), X4) :- splitD(X1, .(X2, X3), X5, X6).
mergesortE(.(X1, .(X2, X3)), X4) :- ','(splitcD(X1, .(X2, X3), X5, X6), mergesortE(X5, X7)).
mergesortE(.(X1, .(X2, X3)), X4) :- ','(splitcD(X1, .(X2, X3), X5, X6), ','(mergesortcE(X5, X7), mergesortE(X6, X8))).
mergesortE(.(X1, .(X2, X3)), .(X4, X5)) :- ','(splitcD(X1, .(X2, X3), X6, X7), ','(mergesortcE(X6, .(X4, X8)), ','(mergesortcE(X7, .(X4, X9)), mergeC(.(X4, X8), X9, X5)))).
mergeC(.(X1, X2), .(X1, X3), .(X1, X4)) :- mergeC(.(X1, X2), X3, X4).
mergesortB(.(X1, .(X2, X3)), X4) :- splitD(X2, X3, X5, X6).
mergesortB(.(X1, .(X2, X3)), X4) :- ','(splitcD(X2, X3, X5, X6), mergesortB(.(X1, X6), X7)).
mergesortB(.(X1, .(X2, X3)), X4) :- ','(splitcD(X2, X3, X5, X6), ','(mergesortcB(.(X1, X6), X7), mergesortE(X5, X8))).
mergesortB(.(X1, .(X2, X3)), X4) :- ','(splitcD(X2, X3, X5, X6), ','(mergesortcB(.(X1, X6), X7), ','(mergesortcE(X5, X8), mergeC(X7, X8, X4)))).

Clauses:

splitcA([], [], []).
splitcA(.(X1, X2), .(X1, X3), X4) :- splitcA(X2, X4, X3).
mergesortcB([], []).
mergesortcB(.(X1, []), .(X1, [])).
mergesortcB(.(X1, .(X2, X3)), X4) :- ','(splitcD(X2, X3, X5, X6), ','(mergesortcB(.(X1, X6), X7), ','(mergesortcE(X5, X8), mergecC(X7, X8, X4)))).
splitcD(X1, X2, .(X1, X3), X4) :- splitcA(X2, X4, X3).
mergesortcE([], []).
mergesortcE(.(X1, []), .(X1, [])).
mergesortcE(.(X1, .(X2, X3)), X4) :- ','(splitcD(X1, .(X2, X3), X5, X6), ','(mergesortcE(X5, []), mergesortcE(X6, X4))).
mergesortcE(.(X1, .(X2, X3)), X4) :- ','(splitcD(X1, .(X2, X3), X5, X6), ','(mergesortcE(X5, X4), mergesortcE(X6, []))).
mergesortcE(.(X1, .(X2, X3)), .(X4, X5)) :- ','(splitcD(X1, .(X2, X3), X6, X7), ','(mergesortcE(X6, .(X4, X8)), ','(mergesortcE(X7, .(X4, X9)), mergecC(.(X4, X8), X9, X5)))).
mergecC([], X1, X1).
mergecC(X1, [], X1).
mergecC(.(X1, X2), .(X1, X3), .(X1, X4)) :- mergecC(.(X1, X2), X3, X4).

Afs:

mergesortB(x1, x2)  =  mergesortB(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
mergesortB_in: (b,f)
splitD_in: (f,b,f,f)
splitA_in: (b,f,f)
splitcD_in: (f,b,f,f)
splitcA_in: (b,f,f)
mergesortcB_in: (b,f)
mergesortcE_in: (b,f) (b,b)
mergecC_in: (b,b,f) (b,b,b)
mergesortE_in: (b,f)
mergeC_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U13_GA(X1, X2, X3, X4, splitD_in_agaa(X2, X3, X5, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_AGAA(X2, X3, X5, X6)
SPLITD_IN_AGAA(X1, X2, .(X1, X3), X4) → U2_AGAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITD_IN_AGAA(X1, X2, .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → U1_GAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U14_GA(X1, X2, X3, X4, splitcD_in_agaa(X2, X3, X5, X6))
U14_GA(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → U15_GA(X1, X2, X3, X4, mergesortB_in_ga(.(X1, X6), X7))
U14_GA(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)
U14_GA(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → U16_GA(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U16_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U17_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X8))
U16_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → MERGESORTE_IN_GA(X5, X8)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U3_GA(X1, X2, X3, X4, splitD_in_agaa(X1, .(X2, X3), X5, X6))
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_AGAA(X1, .(X2, X3), X5, X6)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U5_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X7))
U4_GA(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), .(X4, X5)) → U8_GA(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U8_GA(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U9_GA(X1, X2, X3, X4, X5, X7, mergesortcE_in_ga(X6, .(X4, X8)))
U9_GA(X1, X2, X3, X4, X5, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U10_GA(X1, X2, X3, X4, X5, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U10_GA(X1, X2, X3, X4, X5, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U11_GA(X1, X2, X3, X4, X5, mergeC_in_gga(.(X4, X8), X9, X5))
U10_GA(X1, X2, X3, X4, X5, X8, mergesortcE_out_ga(X7, .(X4, X9))) → MERGEC_IN_GGA(.(X4, X8), X9, X5)
MERGEC_IN_GGA(.(X1, X2), .(X1, X3), .(X1, X4)) → U12_GGA(X1, X2, X3, X4, mergeC_in_gga(.(X1, X2), X3, X4))
MERGEC_IN_GGA(.(X1, X2), .(X1, X3), .(X1, X4)) → MERGEC_IN_GGA(.(X1, X2), X3, X4)
U4_GA(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U7_GA(X1, X2, X3, X4, mergesortE_in_ga(X6, X8))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)
U16_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U18_GA(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
U18_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U19_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U18_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → MERGEC_IN_GGA(X7, X8, X4)

The TRS R consists of the following rules:

splitcD_in_agaa(X1, X2, .(X1, X3), X4) → U26_agaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U21_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U21_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U26_agaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U22_ga(X1, X2, X3, X4, splitcD_in_agaa(X2, X3, X5, X6))
U22_ga(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_in_ga(.(X1, X6), X7))
U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_out_ga(.(X1, X6), X7)) → U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg([], []) → mergesortcE_out_gg([], [])
mergesortcE_in_gg(.(X1, []), .(X1, [])) → mergesortcE_out_gg(.(X1, []), .(X1, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), X4) → U27_gg(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), .(X4, X5)) → U32_gg(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_gg(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
mergesortcE_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U32_ga(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_ga(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_ga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X4, X8), X9, X5))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X3, X4))
U36_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X3, X4)) → mergecC_out_gga(.(X1, X2), .(X1, X3), .(X1, X4))
U35_ga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X4, X8), X9, X5)) → mergesortcE_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_gg(X1, X2, X3, X4, X5, mergecC_in_ggg(.(X4, X8), X9, X5))
mergecC_in_ggg([], X1, X1) → mergecC_out_ggg([], X1, X1)
mergecC_in_ggg(X1, [], X1) → mergecC_out_ggg(X1, [], X1)
mergecC_in_ggg(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_ggg(X1, X2, X3, X4, mergecC_in_ggg(.(X1, X2), X3, X4))
U36_ggg(X1, X2, X3, X4, mergecC_out_ggg(.(X1, X2), X3, X4)) → mergecC_out_ggg(.(X1, X2), .(X1, X3), .(X1, X4))
U35_gg(X1, X2, X3, X4, X5, mergecC_out_ggg(.(X4, X8), X9, X5)) → mergesortcE_out_gg(.(X1, .(X2, X3)), .(X4, X5))
U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, X4))
U29_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, X4)) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, X4))
U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, X4)) → U31_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_ga(X1, X2, X3, X4, mergesortcE_in_ga(X6, X4))
U29_ga(X1, X2, X3, X4, mergesortcE_out_ga(X6, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_ga(X5, X4))
U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_ga(X5, X4)) → U31_ga(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_ga(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X5, X8)) → U25_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U25_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
mergesortB_in_ga(x1, x2)  =  mergesortB_in_ga(x1)
.(x1, x2)  =  .(x2)
splitA_in_gaa(x1, x2, x3)  =  splitA_in_gaa(x1)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U21_gaa(x1, x2, x3, x4, x5)  =  U21_gaa(x2, x5)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U22_ga(x1, x2, x3, x4, x5)  =  U22_ga(x3, x5)
U23_ga(x1, x2, x3, x4, x5, x6, x7)  =  U23_ga(x3, x5, x7)
U24_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U24_ga(x3, x7, x8)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x3, x6, x7)
mergesortcE_in_gg(x1, x2)  =  mergesortcE_in_gg(x1, x2)
mergesortcE_out_gg(x1, x2)  =  mergesortcE_out_gg(x1, x2)
U27_gg(x1, x2, x3, x4, x5)  =  U27_gg(x3, x4, x5)
U28_gg(x1, x2, x3, x4, x5, x6, x7)  =  U28_gg(x3, x4, x6, x7)
U32_gg(x1, x2, x3, x4, x5, x6)  =  U32_gg(x3, x5, x6)
U33_gg(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_gg(x3, x5, x7, x8)
U32_ga(x1, x2, x3, x4, x5, x6)  =  U32_ga(x3, x6)
U33_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_ga(x3, x7, x8)
splitD_in_agaa(x1, x2, x3, x4)  =  splitD_in_agaa(x2)
splitcD_in_agaa(x1, x2, x3, x4)  =  splitcD_in_agaa(x2)
U26_agaa(x1, x2, x3, x4, x5)  =  U26_agaa(x2, x5)
splitcD_out_agaa(x1, x2, x3, x4)  =  splitcD_out_agaa(x2, x3, x4)
U34_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_ga(x3, x8, x9)
U35_ga(x1, x2, x3, x4, x5, x6)  =  U35_ga(x3, x6)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x2, x3, x5)
U34_gg(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_gg(x3, x5, x8, x9)
U35_gg(x1, x2, x3, x4, x5, x6)  =  U35_gg(x3, x5, x6)
mergecC_in_ggg(x1, x2, x3)  =  mergecC_in_ggg(x1, x2, x3)
mergecC_out_ggg(x1, x2, x3)  =  mergecC_out_ggg(x1, x2, x3)
U36_ggg(x1, x2, x3, x4, x5)  =  U36_ggg(x2, x3, x4, x5)
U29_gg(x1, x2, x3, x4, x5)  =  U29_gg(x3, x4, x5)
U30_gg(x1, x2, x3, x4, x5, x6, x7)  =  U30_gg(x3, x4, x6, x7)
U31_gg(x1, x2, x3, x4, x5)  =  U31_gg(x3, x4, x5)
U29_ga(x1, x2, x3, x4, x5)  =  U29_ga(x3, x5)
U30_ga(x1, x2, x3, x4, x5, x6, x7)  =  U30_ga(x3, x6, x7)
U31_ga(x1, x2, x3, x4, x5)  =  U31_ga(x3, x4, x5)
U25_ga(x1, x2, x3, x4, x5)  =  U25_ga(x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergeC_in_gga(x1, x2, x3)  =  mergeC_in_gga(x1, x2)
MERGESORTB_IN_GA(x1, x2)  =  MERGESORTB_IN_GA(x1)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x3, x5)
SPLITD_IN_AGAA(x1, x2, x3, x4)  =  SPLITD_IN_AGAA(x2)
U2_AGAA(x1, x2, x3, x4, x5)  =  U2_AGAA(x2, x5)
SPLITA_IN_GAA(x1, x2, x3)  =  SPLITA_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4, x5)  =  U1_GAA(x2, x5)
U14_GA(x1, x2, x3, x4, x5)  =  U14_GA(x3, x5)
U15_GA(x1, x2, x3, x4, x5)  =  U15_GA(x3, x5)
U16_GA(x1, x2, x3, x4, x5, x6)  =  U16_GA(x3, x5, x6)
U17_GA(x1, x2, x3, x4, x5)  =  U17_GA(x3, x5)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x3, x5)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x3, x5)
U5_GA(x1, x2, x3, x4, x5)  =  U5_GA(x3, x5)
U8_GA(x1, x2, x3, x4, x5, x6)  =  U8_GA(x3, x6)
U9_GA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GA(x3, x6, x7)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x3, x6, x7)
U11_GA(x1, x2, x3, x4, x5, x6)  =  U11_GA(x3, x6)
MERGEC_IN_GGA(x1, x2, x3)  =  MERGEC_IN_GGA(x1, x2)
U12_GGA(x1, x2, x3, x4, x5)  =  U12_GGA(x2, x3, x5)
U6_GA(x1, x2, x3, x4, x5, x6)  =  U6_GA(x3, x5, x6)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x3, x5)
U18_GA(x1, x2, x3, x4, x5, x6)  =  U18_GA(x3, x5, x6)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x3, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U13_GA(X1, X2, X3, X4, splitD_in_agaa(X2, X3, X5, X6))
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_AGAA(X2, X3, X5, X6)
SPLITD_IN_AGAA(X1, X2, .(X1, X3), X4) → U2_AGAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITD_IN_AGAA(X1, X2, .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → U1_GAA(X1, X2, X3, X4, splitA_in_gaa(X2, X4, X3))
SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)
MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U14_GA(X1, X2, X3, X4, splitcD_in_agaa(X2, X3, X5, X6))
U14_GA(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → U15_GA(X1, X2, X3, X4, mergesortB_in_ga(.(X1, X6), X7))
U14_GA(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)
U14_GA(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → U16_GA(X1, X2, X3, X4, X5, mergesortcB_in_ga(.(X1, X6), X7))
U16_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U17_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X8))
U16_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → MERGESORTE_IN_GA(X5, X8)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U3_GA(X1, X2, X3, X4, splitD_in_agaa(X1, .(X2, X3), X5, X6))
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → SPLITD_IN_AGAA(X1, .(X2, X3), X5, X6)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U5_GA(X1, X2, X3, X4, mergesortE_in_ga(X5, X7))
U4_GA(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
MERGESORTE_IN_GA(.(X1, .(X2, X3)), .(X4, X5)) → U8_GA(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U8_GA(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U9_GA(X1, X2, X3, X4, X5, X7, mergesortcE_in_ga(X6, .(X4, X8)))
U9_GA(X1, X2, X3, X4, X5, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U10_GA(X1, X2, X3, X4, X5, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U10_GA(X1, X2, X3, X4, X5, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U11_GA(X1, X2, X3, X4, X5, mergeC_in_gga(.(X4, X8), X9, X5))
U10_GA(X1, X2, X3, X4, X5, X8, mergesortcE_out_ga(X7, .(X4, X9))) → MERGEC_IN_GGA(.(X4, X8), X9, X5)
MERGEC_IN_GGA(.(X1, X2), .(X1, X3), .(X1, X4)) → U12_GGA(X1, X2, X3, X4, mergeC_in_gga(.(X1, X2), X3, X4))
MERGEC_IN_GGA(.(X1, X2), .(X1, X3), .(X1, X4)) → MERGEC_IN_GGA(.(X1, X2), X3, X4)
U4_GA(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → U7_GA(X1, X2, X3, X4, mergesortE_in_ga(X6, X8))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)
U16_GA(X1, X2, X3, X4, X5, mergesortcB_out_ga(.(X1, X6), X7)) → U18_GA(X1, X2, X3, X4, X7, mergesortcE_in_ga(X5, X8))
U18_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → U19_GA(X1, X2, X3, X4, mergeC_in_gga(X7, X8, X4))
U18_GA(X1, X2, X3, X4, X7, mergesortcE_out_ga(X5, X8)) → MERGEC_IN_GGA(X7, X8, X4)

The TRS R consists of the following rules:

splitcD_in_agaa(X1, X2, .(X1, X3), X4) → U26_agaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U21_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U21_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U26_agaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U22_ga(X1, X2, X3, X4, splitcD_in_agaa(X2, X3, X5, X6))
U22_ga(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_in_ga(.(X1, X6), X7))
U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_out_ga(.(X1, X6), X7)) → U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg([], []) → mergesortcE_out_gg([], [])
mergesortcE_in_gg(.(X1, []), .(X1, [])) → mergesortcE_out_gg(.(X1, []), .(X1, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), X4) → U27_gg(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), .(X4, X5)) → U32_gg(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_gg(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
mergesortcE_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U32_ga(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_ga(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_ga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X4, X8), X9, X5))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X3, X4))
U36_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X3, X4)) → mergecC_out_gga(.(X1, X2), .(X1, X3), .(X1, X4))
U35_ga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X4, X8), X9, X5)) → mergesortcE_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_gg(X1, X2, X3, X4, X5, mergecC_in_ggg(.(X4, X8), X9, X5))
mergecC_in_ggg([], X1, X1) → mergecC_out_ggg([], X1, X1)
mergecC_in_ggg(X1, [], X1) → mergecC_out_ggg(X1, [], X1)
mergecC_in_ggg(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_ggg(X1, X2, X3, X4, mergecC_in_ggg(.(X1, X2), X3, X4))
U36_ggg(X1, X2, X3, X4, mergecC_out_ggg(.(X1, X2), X3, X4)) → mergecC_out_ggg(.(X1, X2), .(X1, X3), .(X1, X4))
U35_gg(X1, X2, X3, X4, X5, mergecC_out_ggg(.(X4, X8), X9, X5)) → mergesortcE_out_gg(.(X1, .(X2, X3)), .(X4, X5))
U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, X4))
U29_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, X4)) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, X4))
U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, X4)) → U31_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_ga(X1, X2, X3, X4, mergesortcE_in_ga(X6, X4))
U29_ga(X1, X2, X3, X4, mergesortcE_out_ga(X6, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_ga(X5, X4))
U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_ga(X5, X4)) → U31_ga(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_ga(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X5, X8)) → U25_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U25_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
mergesortB_in_ga(x1, x2)  =  mergesortB_in_ga(x1)
.(x1, x2)  =  .(x2)
splitA_in_gaa(x1, x2, x3)  =  splitA_in_gaa(x1)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U21_gaa(x1, x2, x3, x4, x5)  =  U21_gaa(x2, x5)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U22_ga(x1, x2, x3, x4, x5)  =  U22_ga(x3, x5)
U23_ga(x1, x2, x3, x4, x5, x6, x7)  =  U23_ga(x3, x5, x7)
U24_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U24_ga(x3, x7, x8)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x3, x6, x7)
mergesortcE_in_gg(x1, x2)  =  mergesortcE_in_gg(x1, x2)
mergesortcE_out_gg(x1, x2)  =  mergesortcE_out_gg(x1, x2)
U27_gg(x1, x2, x3, x4, x5)  =  U27_gg(x3, x4, x5)
U28_gg(x1, x2, x3, x4, x5, x6, x7)  =  U28_gg(x3, x4, x6, x7)
U32_gg(x1, x2, x3, x4, x5, x6)  =  U32_gg(x3, x5, x6)
U33_gg(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_gg(x3, x5, x7, x8)
U32_ga(x1, x2, x3, x4, x5, x6)  =  U32_ga(x3, x6)
U33_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_ga(x3, x7, x8)
splitD_in_agaa(x1, x2, x3, x4)  =  splitD_in_agaa(x2)
splitcD_in_agaa(x1, x2, x3, x4)  =  splitcD_in_agaa(x2)
U26_agaa(x1, x2, x3, x4, x5)  =  U26_agaa(x2, x5)
splitcD_out_agaa(x1, x2, x3, x4)  =  splitcD_out_agaa(x2, x3, x4)
U34_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_ga(x3, x8, x9)
U35_ga(x1, x2, x3, x4, x5, x6)  =  U35_ga(x3, x6)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x2, x3, x5)
U34_gg(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_gg(x3, x5, x8, x9)
U35_gg(x1, x2, x3, x4, x5, x6)  =  U35_gg(x3, x5, x6)
mergecC_in_ggg(x1, x2, x3)  =  mergecC_in_ggg(x1, x2, x3)
mergecC_out_ggg(x1, x2, x3)  =  mergecC_out_ggg(x1, x2, x3)
U36_ggg(x1, x2, x3, x4, x5)  =  U36_ggg(x2, x3, x4, x5)
U29_gg(x1, x2, x3, x4, x5)  =  U29_gg(x3, x4, x5)
U30_gg(x1, x2, x3, x4, x5, x6, x7)  =  U30_gg(x3, x4, x6, x7)
U31_gg(x1, x2, x3, x4, x5)  =  U31_gg(x3, x4, x5)
U29_ga(x1, x2, x3, x4, x5)  =  U29_ga(x3, x5)
U30_ga(x1, x2, x3, x4, x5, x6, x7)  =  U30_ga(x3, x6, x7)
U31_ga(x1, x2, x3, x4, x5)  =  U31_ga(x3, x4, x5)
U25_ga(x1, x2, x3, x4, x5)  =  U25_ga(x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergeC_in_gga(x1, x2, x3)  =  mergeC_in_gga(x1, x2)
MERGESORTB_IN_GA(x1, x2)  =  MERGESORTB_IN_GA(x1)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x3, x5)
SPLITD_IN_AGAA(x1, x2, x3, x4)  =  SPLITD_IN_AGAA(x2)
U2_AGAA(x1, x2, x3, x4, x5)  =  U2_AGAA(x2, x5)
SPLITA_IN_GAA(x1, x2, x3)  =  SPLITA_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4, x5)  =  U1_GAA(x2, x5)
U14_GA(x1, x2, x3, x4, x5)  =  U14_GA(x3, x5)
U15_GA(x1, x2, x3, x4, x5)  =  U15_GA(x3, x5)
U16_GA(x1, x2, x3, x4, x5, x6)  =  U16_GA(x3, x5, x6)
U17_GA(x1, x2, x3, x4, x5)  =  U17_GA(x3, x5)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x3, x5)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x3, x5)
U5_GA(x1, x2, x3, x4, x5)  =  U5_GA(x3, x5)
U8_GA(x1, x2, x3, x4, x5, x6)  =  U8_GA(x3, x6)
U9_GA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GA(x3, x6, x7)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x3, x6, x7)
U11_GA(x1, x2, x3, x4, x5, x6)  =  U11_GA(x3, x6)
MERGEC_IN_GGA(x1, x2, x3)  =  MERGEC_IN_GGA(x1, x2)
U12_GGA(x1, x2, x3, x4, x5)  =  U12_GGA(x2, x3, x5)
U6_GA(x1, x2, x3, x4, x5, x6)  =  U6_GA(x3, x5, x6)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x3, x5)
U18_GA(x1, x2, x3, x4, x5, x6)  =  U18_GA(x3, x5, x6)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x3, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 22 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGEC_IN_GGA(.(X1, X2), .(X1, X3), .(X1, X4)) → MERGEC_IN_GGA(.(X1, X2), X3, X4)

The TRS R consists of the following rules:

splitcD_in_agaa(X1, X2, .(X1, X3), X4) → U26_agaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U21_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U21_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U26_agaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U22_ga(X1, X2, X3, X4, splitcD_in_agaa(X2, X3, X5, X6))
U22_ga(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_in_ga(.(X1, X6), X7))
U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_out_ga(.(X1, X6), X7)) → U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg([], []) → mergesortcE_out_gg([], [])
mergesortcE_in_gg(.(X1, []), .(X1, [])) → mergesortcE_out_gg(.(X1, []), .(X1, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), X4) → U27_gg(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), .(X4, X5)) → U32_gg(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_gg(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
mergesortcE_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U32_ga(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_ga(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_ga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X4, X8), X9, X5))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X3, X4))
U36_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X3, X4)) → mergecC_out_gga(.(X1, X2), .(X1, X3), .(X1, X4))
U35_ga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X4, X8), X9, X5)) → mergesortcE_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_gg(X1, X2, X3, X4, X5, mergecC_in_ggg(.(X4, X8), X9, X5))
mergecC_in_ggg([], X1, X1) → mergecC_out_ggg([], X1, X1)
mergecC_in_ggg(X1, [], X1) → mergecC_out_ggg(X1, [], X1)
mergecC_in_ggg(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_ggg(X1, X2, X3, X4, mergecC_in_ggg(.(X1, X2), X3, X4))
U36_ggg(X1, X2, X3, X4, mergecC_out_ggg(.(X1, X2), X3, X4)) → mergecC_out_ggg(.(X1, X2), .(X1, X3), .(X1, X4))
U35_gg(X1, X2, X3, X4, X5, mergecC_out_ggg(.(X4, X8), X9, X5)) → mergesortcE_out_gg(.(X1, .(X2, X3)), .(X4, X5))
U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, X4))
U29_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, X4)) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, X4))
U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, X4)) → U31_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_ga(X1, X2, X3, X4, mergesortcE_in_ga(X6, X4))
U29_ga(X1, X2, X3, X4, mergesortcE_out_ga(X6, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_ga(X5, X4))
U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_ga(X5, X4)) → U31_ga(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_ga(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X5, X8)) → U25_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U25_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U21_gaa(x1, x2, x3, x4, x5)  =  U21_gaa(x2, x5)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U22_ga(x1, x2, x3, x4, x5)  =  U22_ga(x3, x5)
U23_ga(x1, x2, x3, x4, x5, x6, x7)  =  U23_ga(x3, x5, x7)
U24_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U24_ga(x3, x7, x8)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x3, x6, x7)
mergesortcE_in_gg(x1, x2)  =  mergesortcE_in_gg(x1, x2)
mergesortcE_out_gg(x1, x2)  =  mergesortcE_out_gg(x1, x2)
U27_gg(x1, x2, x3, x4, x5)  =  U27_gg(x3, x4, x5)
U28_gg(x1, x2, x3, x4, x5, x6, x7)  =  U28_gg(x3, x4, x6, x7)
U32_gg(x1, x2, x3, x4, x5, x6)  =  U32_gg(x3, x5, x6)
U33_gg(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_gg(x3, x5, x7, x8)
U32_ga(x1, x2, x3, x4, x5, x6)  =  U32_ga(x3, x6)
U33_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_ga(x3, x7, x8)
splitcD_in_agaa(x1, x2, x3, x4)  =  splitcD_in_agaa(x2)
U26_agaa(x1, x2, x3, x4, x5)  =  U26_agaa(x2, x5)
splitcD_out_agaa(x1, x2, x3, x4)  =  splitcD_out_agaa(x2, x3, x4)
U34_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_ga(x3, x8, x9)
U35_ga(x1, x2, x3, x4, x5, x6)  =  U35_ga(x3, x6)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x2, x3, x5)
U34_gg(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_gg(x3, x5, x8, x9)
U35_gg(x1, x2, x3, x4, x5, x6)  =  U35_gg(x3, x5, x6)
mergecC_in_ggg(x1, x2, x3)  =  mergecC_in_ggg(x1, x2, x3)
mergecC_out_ggg(x1, x2, x3)  =  mergecC_out_ggg(x1, x2, x3)
U36_ggg(x1, x2, x3, x4, x5)  =  U36_ggg(x2, x3, x4, x5)
U29_gg(x1, x2, x3, x4, x5)  =  U29_gg(x3, x4, x5)
U30_gg(x1, x2, x3, x4, x5, x6, x7)  =  U30_gg(x3, x4, x6, x7)
U31_gg(x1, x2, x3, x4, x5)  =  U31_gg(x3, x4, x5)
U29_ga(x1, x2, x3, x4, x5)  =  U29_ga(x3, x5)
U30_ga(x1, x2, x3, x4, x5, x6, x7)  =  U30_ga(x3, x6, x7)
U31_ga(x1, x2, x3, x4, x5)  =  U31_ga(x3, x4, x5)
U25_ga(x1, x2, x3, x4, x5)  =  U25_ga(x3, x5)
MERGEC_IN_GGA(x1, x2, x3)  =  MERGEC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGEC_IN_GGA(.(X1, X2), .(X1, X3), .(X1, X4)) → MERGEC_IN_GGA(.(X1, X2), X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
MERGEC_IN_GGA(x1, x2, x3)  =  MERGEC_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MERGEC_IN_GGA(.(X2), .(X3)) → MERGEC_IN_GGA(.(X2), X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MERGEC_IN_GGA(.(X2), .(X3)) → MERGEC_IN_GGA(.(X2), X3)
    The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)

The TRS R consists of the following rules:

splitcD_in_agaa(X1, X2, .(X1, X3), X4) → U26_agaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U21_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U21_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U26_agaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U22_ga(X1, X2, X3, X4, splitcD_in_agaa(X2, X3, X5, X6))
U22_ga(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_in_ga(.(X1, X6), X7))
U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_out_ga(.(X1, X6), X7)) → U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg([], []) → mergesortcE_out_gg([], [])
mergesortcE_in_gg(.(X1, []), .(X1, [])) → mergesortcE_out_gg(.(X1, []), .(X1, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), X4) → U27_gg(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), .(X4, X5)) → U32_gg(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_gg(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
mergesortcE_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U32_ga(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_ga(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_ga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X4, X8), X9, X5))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X3, X4))
U36_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X3, X4)) → mergecC_out_gga(.(X1, X2), .(X1, X3), .(X1, X4))
U35_ga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X4, X8), X9, X5)) → mergesortcE_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_gg(X1, X2, X3, X4, X5, mergecC_in_ggg(.(X4, X8), X9, X5))
mergecC_in_ggg([], X1, X1) → mergecC_out_ggg([], X1, X1)
mergecC_in_ggg(X1, [], X1) → mergecC_out_ggg(X1, [], X1)
mergecC_in_ggg(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_ggg(X1, X2, X3, X4, mergecC_in_ggg(.(X1, X2), X3, X4))
U36_ggg(X1, X2, X3, X4, mergecC_out_ggg(.(X1, X2), X3, X4)) → mergecC_out_ggg(.(X1, X2), .(X1, X3), .(X1, X4))
U35_gg(X1, X2, X3, X4, X5, mergecC_out_ggg(.(X4, X8), X9, X5)) → mergesortcE_out_gg(.(X1, .(X2, X3)), .(X4, X5))
U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, X4))
U29_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, X4)) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, X4))
U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, X4)) → U31_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_ga(X1, X2, X3, X4, mergesortcE_in_ga(X6, X4))
U29_ga(X1, X2, X3, X4, mergesortcE_out_ga(X6, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_ga(X5, X4))
U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_ga(X5, X4)) → U31_ga(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_ga(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X5, X8)) → U25_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U25_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U21_gaa(x1, x2, x3, x4, x5)  =  U21_gaa(x2, x5)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U22_ga(x1, x2, x3, x4, x5)  =  U22_ga(x3, x5)
U23_ga(x1, x2, x3, x4, x5, x6, x7)  =  U23_ga(x3, x5, x7)
U24_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U24_ga(x3, x7, x8)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x3, x6, x7)
mergesortcE_in_gg(x1, x2)  =  mergesortcE_in_gg(x1, x2)
mergesortcE_out_gg(x1, x2)  =  mergesortcE_out_gg(x1, x2)
U27_gg(x1, x2, x3, x4, x5)  =  U27_gg(x3, x4, x5)
U28_gg(x1, x2, x3, x4, x5, x6, x7)  =  U28_gg(x3, x4, x6, x7)
U32_gg(x1, x2, x3, x4, x5, x6)  =  U32_gg(x3, x5, x6)
U33_gg(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_gg(x3, x5, x7, x8)
U32_ga(x1, x2, x3, x4, x5, x6)  =  U32_ga(x3, x6)
U33_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_ga(x3, x7, x8)
splitcD_in_agaa(x1, x2, x3, x4)  =  splitcD_in_agaa(x2)
U26_agaa(x1, x2, x3, x4, x5)  =  U26_agaa(x2, x5)
splitcD_out_agaa(x1, x2, x3, x4)  =  splitcD_out_agaa(x2, x3, x4)
U34_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_ga(x3, x8, x9)
U35_ga(x1, x2, x3, x4, x5, x6)  =  U35_ga(x3, x6)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x2, x3, x5)
U34_gg(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_gg(x3, x5, x8, x9)
U35_gg(x1, x2, x3, x4, x5, x6)  =  U35_gg(x3, x5, x6)
mergecC_in_ggg(x1, x2, x3)  =  mergecC_in_ggg(x1, x2, x3)
mergecC_out_ggg(x1, x2, x3)  =  mergecC_out_ggg(x1, x2, x3)
U36_ggg(x1, x2, x3, x4, x5)  =  U36_ggg(x2, x3, x4, x5)
U29_gg(x1, x2, x3, x4, x5)  =  U29_gg(x3, x4, x5)
U30_gg(x1, x2, x3, x4, x5, x6, x7)  =  U30_gg(x3, x4, x6, x7)
U31_gg(x1, x2, x3, x4, x5)  =  U31_gg(x3, x4, x5)
U29_ga(x1, x2, x3, x4, x5)  =  U29_ga(x3, x5)
U30_ga(x1, x2, x3, x4, x5, x6, x7)  =  U30_ga(x3, x6, x7)
U31_ga(x1, x2, x3, x4, x5)  =  U31_ga(x3, x4, x5)
U25_ga(x1, x2, x3, x4, x5)  =  U25_ga(x3, x5)
SPLITA_IN_GAA(x1, x2, x3)  =  SPLITA_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

SPLITA_IN_GAA(.(X1, X2), .(X1, X3), X4) → SPLITA_IN_GAA(X2, X4, X3)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
SPLITA_IN_GAA(x1, x2, x3)  =  SPLITA_IN_GAA(x1)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

SPLITA_IN_GAA(.(X2)) → SPLITA_IN_GAA(X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SPLITA_IN_GAA(.(X2)) → SPLITA_IN_GAA(X2)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
U4_GA(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)

The TRS R consists of the following rules:

splitcD_in_agaa(X1, X2, .(X1, X3), X4) → U26_agaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U21_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U21_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U26_agaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U22_ga(X1, X2, X3, X4, splitcD_in_agaa(X2, X3, X5, X6))
U22_ga(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_in_ga(.(X1, X6), X7))
U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_out_ga(.(X1, X6), X7)) → U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg([], []) → mergesortcE_out_gg([], [])
mergesortcE_in_gg(.(X1, []), .(X1, [])) → mergesortcE_out_gg(.(X1, []), .(X1, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), X4) → U27_gg(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), .(X4, X5)) → U32_gg(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_gg(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
mergesortcE_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U32_ga(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_ga(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_ga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X4, X8), X9, X5))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X3, X4))
U36_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X3, X4)) → mergecC_out_gga(.(X1, X2), .(X1, X3), .(X1, X4))
U35_ga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X4, X8), X9, X5)) → mergesortcE_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_gg(X1, X2, X3, X4, X5, mergecC_in_ggg(.(X4, X8), X9, X5))
mergecC_in_ggg([], X1, X1) → mergecC_out_ggg([], X1, X1)
mergecC_in_ggg(X1, [], X1) → mergecC_out_ggg(X1, [], X1)
mergecC_in_ggg(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_ggg(X1, X2, X3, X4, mergecC_in_ggg(.(X1, X2), X3, X4))
U36_ggg(X1, X2, X3, X4, mergecC_out_ggg(.(X1, X2), X3, X4)) → mergecC_out_ggg(.(X1, X2), .(X1, X3), .(X1, X4))
U35_gg(X1, X2, X3, X4, X5, mergecC_out_ggg(.(X4, X8), X9, X5)) → mergesortcE_out_gg(.(X1, .(X2, X3)), .(X4, X5))
U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, X4))
U29_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, X4)) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, X4))
U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, X4)) → U31_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_ga(X1, X2, X3, X4, mergesortcE_in_ga(X6, X4))
U29_ga(X1, X2, X3, X4, mergesortcE_out_ga(X6, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_ga(X5, X4))
U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_ga(X5, X4)) → U31_ga(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_ga(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X5, X8)) → U25_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U25_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U21_gaa(x1, x2, x3, x4, x5)  =  U21_gaa(x2, x5)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U22_ga(x1, x2, x3, x4, x5)  =  U22_ga(x3, x5)
U23_ga(x1, x2, x3, x4, x5, x6, x7)  =  U23_ga(x3, x5, x7)
U24_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U24_ga(x3, x7, x8)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x3, x6, x7)
mergesortcE_in_gg(x1, x2)  =  mergesortcE_in_gg(x1, x2)
mergesortcE_out_gg(x1, x2)  =  mergesortcE_out_gg(x1, x2)
U27_gg(x1, x2, x3, x4, x5)  =  U27_gg(x3, x4, x5)
U28_gg(x1, x2, x3, x4, x5, x6, x7)  =  U28_gg(x3, x4, x6, x7)
U32_gg(x1, x2, x3, x4, x5, x6)  =  U32_gg(x3, x5, x6)
U33_gg(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_gg(x3, x5, x7, x8)
U32_ga(x1, x2, x3, x4, x5, x6)  =  U32_ga(x3, x6)
U33_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_ga(x3, x7, x8)
splitcD_in_agaa(x1, x2, x3, x4)  =  splitcD_in_agaa(x2)
U26_agaa(x1, x2, x3, x4, x5)  =  U26_agaa(x2, x5)
splitcD_out_agaa(x1, x2, x3, x4)  =  splitcD_out_agaa(x2, x3, x4)
U34_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_ga(x3, x8, x9)
U35_ga(x1, x2, x3, x4, x5, x6)  =  U35_ga(x3, x6)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x2, x3, x5)
U34_gg(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_gg(x3, x5, x8, x9)
U35_gg(x1, x2, x3, x4, x5, x6)  =  U35_gg(x3, x5, x6)
mergecC_in_ggg(x1, x2, x3)  =  mergecC_in_ggg(x1, x2, x3)
mergecC_out_ggg(x1, x2, x3)  =  mergecC_out_ggg(x1, x2, x3)
U36_ggg(x1, x2, x3, x4, x5)  =  U36_ggg(x2, x3, x4, x5)
U29_gg(x1, x2, x3, x4, x5)  =  U29_gg(x3, x4, x5)
U30_gg(x1, x2, x3, x4, x5, x6, x7)  =  U30_gg(x3, x4, x6, x7)
U31_gg(x1, x2, x3, x4, x5)  =  U31_gg(x3, x4, x5)
U29_ga(x1, x2, x3, x4, x5)  =  U29_ga(x3, x5)
U30_ga(x1, x2, x3, x4, x5, x6, x7)  =  U30_ga(x3, x6, x7)
U31_ga(x1, x2, x3, x4, x5)  =  U31_ga(x3, x4, x5)
U25_ga(x1, x2, x3, x4, x5)  =  U25_ga(x3, x5)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x3, x5)
U6_GA(x1, x2, x3, x4, x5, x6)  =  U6_GA(x3, x5, x6)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTE_IN_GA(.(X1, .(X2, X3)), X4) → U4_GA(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U4_GA(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → MERGESORTE_IN_GA(X5, X7)
U4_GA(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U6_GA(X1, X2, X3, X4, X6, mergesortcE_in_ga(X5, X7))
U6_GA(X1, X2, X3, X4, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6, X8)

The TRS R consists of the following rules:

splitcD_in_agaa(X1, X2, .(X1, X3), X4) → U26_agaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
mergesortcE_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U32_ga(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U26_agaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X1, X2, .(X1, X3), X4)
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_ga(X5, X4))
U32_ga(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U21_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_ga(X1, X2, X3, X4, mergesortcE_in_ga(X6, X4))
U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_ga(X5, X4)) → U31_ga(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U21_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
mergesortcE_in_gg([], []) → mergesortcE_out_gg([], [])
mergesortcE_in_gg(.(X1, .(X2, X3)), X4) → U27_gg(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U29_ga(X1, X2, X3, X4, mergesortcE_out_ga(X6, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U31_ga(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_ga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X4, X8), X9, X5))
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, X4))
U35_ga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X4, X8), X9, X5)) → mergesortcE_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, X4))
U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, X4)) → U31_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X3, X4))
U29_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, X4)) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
mergesortcE_in_gg(.(X1, []), .(X1, [])) → mergesortcE_out_gg(.(X1, []), .(X1, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), .(X4, X5)) → U32_gg(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U31_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U36_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X3, X4)) → mergecC_out_gga(.(X1, X2), .(X1, X3), .(X1, X4))
U32_gg(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_gg(X1, X2, X3, X4, X5, mergecC_in_ggg(.(X4, X8), X9, X5))
U35_gg(X1, X2, X3, X4, X5, mergecC_out_ggg(.(X4, X8), X9, X5)) → mergesortcE_out_gg(.(X1, .(X2, X3)), .(X4, X5))
mergecC_in_ggg(X1, [], X1) → mergecC_out_ggg(X1, [], X1)
mergecC_in_ggg(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_ggg(X1, X2, X3, X4, mergecC_in_ggg(.(X1, X2), X3, X4))
U36_ggg(X1, X2, X3, X4, mergecC_out_ggg(.(X1, X2), X3, X4)) → mergecC_out_ggg(.(X1, X2), .(X1, X3), .(X1, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U21_gaa(x1, x2, x3, x4, x5)  =  U21_gaa(x2, x5)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x3, x6, x7)
mergesortcE_in_gg(x1, x2)  =  mergesortcE_in_gg(x1, x2)
mergesortcE_out_gg(x1, x2)  =  mergesortcE_out_gg(x1, x2)
U27_gg(x1, x2, x3, x4, x5)  =  U27_gg(x3, x4, x5)
U28_gg(x1, x2, x3, x4, x5, x6, x7)  =  U28_gg(x3, x4, x6, x7)
U32_gg(x1, x2, x3, x4, x5, x6)  =  U32_gg(x3, x5, x6)
U33_gg(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_gg(x3, x5, x7, x8)
U32_ga(x1, x2, x3, x4, x5, x6)  =  U32_ga(x3, x6)
U33_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_ga(x3, x7, x8)
splitcD_in_agaa(x1, x2, x3, x4)  =  splitcD_in_agaa(x2)
U26_agaa(x1, x2, x3, x4, x5)  =  U26_agaa(x2, x5)
splitcD_out_agaa(x1, x2, x3, x4)  =  splitcD_out_agaa(x2, x3, x4)
U34_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_ga(x3, x8, x9)
U35_ga(x1, x2, x3, x4, x5, x6)  =  U35_ga(x3, x6)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x2, x3, x5)
U34_gg(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_gg(x3, x5, x8, x9)
U35_gg(x1, x2, x3, x4, x5, x6)  =  U35_gg(x3, x5, x6)
mergecC_in_ggg(x1, x2, x3)  =  mergecC_in_ggg(x1, x2, x3)
mergecC_out_ggg(x1, x2, x3)  =  mergecC_out_ggg(x1, x2, x3)
U36_ggg(x1, x2, x3, x4, x5)  =  U36_ggg(x2, x3, x4, x5)
U29_gg(x1, x2, x3, x4, x5)  =  U29_gg(x3, x4, x5)
U30_gg(x1, x2, x3, x4, x5, x6, x7)  =  U30_gg(x3, x4, x6, x7)
U31_gg(x1, x2, x3, x4, x5)  =  U31_gg(x3, x4, x5)
U29_ga(x1, x2, x3, x4, x5)  =  U29_ga(x3, x5)
U30_ga(x1, x2, x3, x4, x5, x6, x7)  =  U30_ga(x3, x6, x7)
U31_ga(x1, x2, x3, x4, x5)  =  U31_ga(x3, x4, x5)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x3, x5)
U6_GA(x1, x2, x3, x4, x5, x6)  =  U6_GA(x3, x5, x6)

We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MERGESORTE_IN_GA(.(.(X3))) → U4_GA(X3, splitcD_in_agaa(.(X3)))
U4_GA(X3, splitcD_out_agaa(.(X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X3, splitcD_out_agaa(.(X3), X5, X6)) → U6_GA(X3, X6, mergesortcE_in_ga(X5))
U6_GA(X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)

The TRS R consists of the following rules:

splitcD_in_agaa(X2) → U26_agaa(X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.([])) → mergesortcE_out_ga(.([]), .([]))
mergesortcE_in_ga(.(.(X3))) → U27_ga(X3, splitcD_in_agaa(.(X3)))
mergesortcE_in_ga(.(.(X3))) → U32_ga(X3, splitcD_in_agaa(.(X3)))
U26_agaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X2, .(X3), X4)
U27_ga(X3, splitcD_out_agaa(.(X3), X5, X6)) → U28_ga(X3, X6, mergesortcE_in_gg(X5, []))
U27_ga(X3, splitcD_out_agaa(.(X3), X5, X6)) → U30_ga(X3, X6, mergesortcE_in_ga(X5))
U32_ga(X3, splitcD_out_agaa(.(X3), X6, X7)) → U33_ga(X3, X7, mergesortcE_in_ga(X6))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X2)) → U21_gaa(X2, splitcA_in_gaa(X2))
U28_ga(X3, X6, mergesortcE_out_gg(X5, [])) → U29_ga(X3, mergesortcE_in_ga(X6))
U30_ga(X3, X6, mergesortcE_out_ga(X5, X4)) → U31_ga(X3, X4, mergesortcE_in_gg(X6, []))
U33_ga(X3, X7, mergesortcE_out_ga(X6, .(X8))) → U34_ga(X3, X8, mergesortcE_in_ga(X7))
U21_gaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X2), .(X3), X4)
mergesortcE_in_gg([], []) → mergesortcE_out_gg([], [])
mergesortcE_in_gg(.(.(X3)), X4) → U27_gg(X3, X4, splitcD_in_agaa(.(X3)))
U29_ga(X3, mergesortcE_out_ga(X6, X4)) → mergesortcE_out_ga(.(.(X3)), X4)
U31_ga(X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_ga(.(.(X3)), X4)
U34_ga(X3, X8, mergesortcE_out_ga(X7, .(X9))) → U35_ga(X3, mergecC_in_gga(.(X8), X9))
U27_gg(X3, X4, splitcD_out_agaa(.(X3), X5, X6)) → U28_gg(X3, X4, X6, mergesortcE_in_gg(X5, []))
U27_gg(X3, X4, splitcD_out_agaa(.(X3), X5, X6)) → U30_gg(X3, X4, X6, mergesortcE_in_gg(X5, X4))
U35_ga(X3, mergecC_out_gga(.(X8), X9, X5)) → mergesortcE_out_ga(.(.(X3)), .(X5))
U28_gg(X3, X4, X6, mergesortcE_out_gg(X5, [])) → U29_gg(X3, X4, mergesortcE_in_gg(X6, X4))
U30_gg(X3, X4, X6, mergesortcE_out_gg(X5, X4)) → U31_gg(X3, X4, mergesortcE_in_gg(X6, []))
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X2), .(X3)) → U36_gga(X2, X3, mergecC_in_gga(.(X2), X3))
U29_gg(X3, X4, mergesortcE_out_gg(X6, X4)) → mergesortcE_out_gg(.(.(X3)), X4)
mergesortcE_in_gg(.([]), .([])) → mergesortcE_out_gg(.([]), .([]))
mergesortcE_in_gg(.(.(X3)), .(X5)) → U32_gg(X3, X5, splitcD_in_agaa(.(X3)))
U31_gg(X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_gg(.(.(X3)), X4)
U36_gga(X2, X3, mergecC_out_gga(.(X2), X3, X4)) → mergecC_out_gga(.(X2), .(X3), .(X4))
U32_gg(X3, X5, splitcD_out_agaa(.(X3), X6, X7)) → U33_gg(X3, X5, X7, mergesortcE_in_ga(X6))
U33_gg(X3, X5, X7, mergesortcE_out_ga(X6, .(X8))) → U34_gg(X3, X5, X8, mergesortcE_in_ga(X7))
U34_gg(X3, X5, X8, mergesortcE_out_ga(X7, .(X9))) → U35_gg(X3, X5, mergecC_in_ggg(.(X8), X9, X5))
U35_gg(X3, X5, mergecC_out_ggg(.(X8), X9, X5)) → mergesortcE_out_gg(.(.(X3)), .(X5))
mergecC_in_ggg(X1, [], X1) → mergecC_out_ggg(X1, [], X1)
mergecC_in_ggg(.(X2), .(X3), .(X4)) → U36_ggg(X2, X3, X4, mergecC_in_ggg(.(X2), X3, X4))
U36_ggg(X2, X3, X4, mergecC_out_ggg(.(X2), X3, X4)) → mergecC_out_ggg(.(X2), .(X3), .(X4))

The set Q consists of the following terms:

splitcD_in_agaa(x0)
mergesortcE_in_ga(x0)
U26_agaa(x0, x1)
U27_ga(x0, x1)
U32_ga(x0, x1)
splitcA_in_gaa(x0)
U28_ga(x0, x1, x2)
U30_ga(x0, x1, x2)
U33_ga(x0, x1, x2)
U21_gaa(x0, x1)
mergesortcE_in_gg(x0, x1)
U29_ga(x0, x1)
U31_ga(x0, x1, x2)
U34_ga(x0, x1, x2)
U27_gg(x0, x1, x2)
U35_ga(x0, x1)
U28_gg(x0, x1, x2, x3)
U30_gg(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U29_gg(x0, x1, x2)
U31_gg(x0, x1, x2)
U36_gga(x0, x1, x2)
U32_gg(x0, x1, x2)
U33_gg(x0, x1, x2, x3)
U34_gg(x0, x1, x2, x3)
U35_gg(x0, x1, x2)
mergecC_in_ggg(x0, x1, x2)
U36_ggg(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(26) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule MERGESORTE_IN_GA(.(.(X3))) → U4_GA(X3, splitcD_in_agaa(.(X3))) at position [1] we obtained the following new rules [LPAR04]:

MERGESORTE_IN_GA(.(.(X3))) → U4_GA(X3, U26_agaa(.(X3), splitcA_in_gaa(.(X3))))

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U4_GA(X3, splitcD_out_agaa(.(X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X3, splitcD_out_agaa(.(X3), X5, X6)) → U6_GA(X3, X6, mergesortcE_in_ga(X5))
U6_GA(X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)
MERGESORTE_IN_GA(.(.(X3))) → U4_GA(X3, U26_agaa(.(X3), splitcA_in_gaa(.(X3))))

The TRS R consists of the following rules:

splitcD_in_agaa(X2) → U26_agaa(X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.([])) → mergesortcE_out_ga(.([]), .([]))
mergesortcE_in_ga(.(.(X3))) → U27_ga(X3, splitcD_in_agaa(.(X3)))
mergesortcE_in_ga(.(.(X3))) → U32_ga(X3, splitcD_in_agaa(.(X3)))
U26_agaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X2, .(X3), X4)
U27_ga(X3, splitcD_out_agaa(.(X3), X5, X6)) → U28_ga(X3, X6, mergesortcE_in_gg(X5, []))
U27_ga(X3, splitcD_out_agaa(.(X3), X5, X6)) → U30_ga(X3, X6, mergesortcE_in_ga(X5))
U32_ga(X3, splitcD_out_agaa(.(X3), X6, X7)) → U33_ga(X3, X7, mergesortcE_in_ga(X6))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X2)) → U21_gaa(X2, splitcA_in_gaa(X2))
U28_ga(X3, X6, mergesortcE_out_gg(X5, [])) → U29_ga(X3, mergesortcE_in_ga(X6))
U30_ga(X3, X6, mergesortcE_out_ga(X5, X4)) → U31_ga(X3, X4, mergesortcE_in_gg(X6, []))
U33_ga(X3, X7, mergesortcE_out_ga(X6, .(X8))) → U34_ga(X3, X8, mergesortcE_in_ga(X7))
U21_gaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X2), .(X3), X4)
mergesortcE_in_gg([], []) → mergesortcE_out_gg([], [])
mergesortcE_in_gg(.(.(X3)), X4) → U27_gg(X3, X4, splitcD_in_agaa(.(X3)))
U29_ga(X3, mergesortcE_out_ga(X6, X4)) → mergesortcE_out_ga(.(.(X3)), X4)
U31_ga(X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_ga(.(.(X3)), X4)
U34_ga(X3, X8, mergesortcE_out_ga(X7, .(X9))) → U35_ga(X3, mergecC_in_gga(.(X8), X9))
U27_gg(X3, X4, splitcD_out_agaa(.(X3), X5, X6)) → U28_gg(X3, X4, X6, mergesortcE_in_gg(X5, []))
U27_gg(X3, X4, splitcD_out_agaa(.(X3), X5, X6)) → U30_gg(X3, X4, X6, mergesortcE_in_gg(X5, X4))
U35_ga(X3, mergecC_out_gga(.(X8), X9, X5)) → mergesortcE_out_ga(.(.(X3)), .(X5))
U28_gg(X3, X4, X6, mergesortcE_out_gg(X5, [])) → U29_gg(X3, X4, mergesortcE_in_gg(X6, X4))
U30_gg(X3, X4, X6, mergesortcE_out_gg(X5, X4)) → U31_gg(X3, X4, mergesortcE_in_gg(X6, []))
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X2), .(X3)) → U36_gga(X2, X3, mergecC_in_gga(.(X2), X3))
U29_gg(X3, X4, mergesortcE_out_gg(X6, X4)) → mergesortcE_out_gg(.(.(X3)), X4)
mergesortcE_in_gg(.([]), .([])) → mergesortcE_out_gg(.([]), .([]))
mergesortcE_in_gg(.(.(X3)), .(X5)) → U32_gg(X3, X5, splitcD_in_agaa(.(X3)))
U31_gg(X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_gg(.(.(X3)), X4)
U36_gga(X2, X3, mergecC_out_gga(.(X2), X3, X4)) → mergecC_out_gga(.(X2), .(X3), .(X4))
U32_gg(X3, X5, splitcD_out_agaa(.(X3), X6, X7)) → U33_gg(X3, X5, X7, mergesortcE_in_ga(X6))
U33_gg(X3, X5, X7, mergesortcE_out_ga(X6, .(X8))) → U34_gg(X3, X5, X8, mergesortcE_in_ga(X7))
U34_gg(X3, X5, X8, mergesortcE_out_ga(X7, .(X9))) → U35_gg(X3, X5, mergecC_in_ggg(.(X8), X9, X5))
U35_gg(X3, X5, mergecC_out_ggg(.(X8), X9, X5)) → mergesortcE_out_gg(.(.(X3)), .(X5))
mergecC_in_ggg(X1, [], X1) → mergecC_out_ggg(X1, [], X1)
mergecC_in_ggg(.(X2), .(X3), .(X4)) → U36_ggg(X2, X3, X4, mergecC_in_ggg(.(X2), X3, X4))
U36_ggg(X2, X3, X4, mergecC_out_ggg(.(X2), X3, X4)) → mergecC_out_ggg(.(X2), .(X3), .(X4))

The set Q consists of the following terms:

splitcD_in_agaa(x0)
mergesortcE_in_ga(x0)
U26_agaa(x0, x1)
U27_ga(x0, x1)
U32_ga(x0, x1)
splitcA_in_gaa(x0)
U28_ga(x0, x1, x2)
U30_ga(x0, x1, x2)
U33_ga(x0, x1, x2)
U21_gaa(x0, x1)
mergesortcE_in_gg(x0, x1)
U29_ga(x0, x1)
U31_ga(x0, x1, x2)
U34_ga(x0, x1, x2)
U27_gg(x0, x1, x2)
U35_ga(x0, x1)
U28_gg(x0, x1, x2, x3)
U30_gg(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U29_gg(x0, x1, x2)
U31_gg(x0, x1, x2)
U36_gga(x0, x1, x2)
U32_gg(x0, x1, x2)
U33_gg(x0, x1, x2, x3)
U34_gg(x0, x1, x2, x3)
U35_gg(x0, x1, x2)
mergecC_in_ggg(x0, x1, x2)
U36_ggg(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(28) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule MERGESORTE_IN_GA(.(.(X3))) → U4_GA(X3, U26_agaa(.(X3), splitcA_in_gaa(.(X3)))) at position [1,1] we obtained the following new rules [LPAR04]:

MERGESORTE_IN_GA(.(.(X3))) → U4_GA(X3, U26_agaa(.(X3), U21_gaa(X3, splitcA_in_gaa(X3))))

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U4_GA(X3, splitcD_out_agaa(.(X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X3, splitcD_out_agaa(.(X3), X5, X6)) → U6_GA(X3, X6, mergesortcE_in_ga(X5))
U6_GA(X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)
MERGESORTE_IN_GA(.(.(X3))) → U4_GA(X3, U26_agaa(.(X3), U21_gaa(X3, splitcA_in_gaa(X3))))

The TRS R consists of the following rules:

splitcD_in_agaa(X2) → U26_agaa(X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.([])) → mergesortcE_out_ga(.([]), .([]))
mergesortcE_in_ga(.(.(X3))) → U27_ga(X3, splitcD_in_agaa(.(X3)))
mergesortcE_in_ga(.(.(X3))) → U32_ga(X3, splitcD_in_agaa(.(X3)))
U26_agaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X2, .(X3), X4)
U27_ga(X3, splitcD_out_agaa(.(X3), X5, X6)) → U28_ga(X3, X6, mergesortcE_in_gg(X5, []))
U27_ga(X3, splitcD_out_agaa(.(X3), X5, X6)) → U30_ga(X3, X6, mergesortcE_in_ga(X5))
U32_ga(X3, splitcD_out_agaa(.(X3), X6, X7)) → U33_ga(X3, X7, mergesortcE_in_ga(X6))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X2)) → U21_gaa(X2, splitcA_in_gaa(X2))
U28_ga(X3, X6, mergesortcE_out_gg(X5, [])) → U29_ga(X3, mergesortcE_in_ga(X6))
U30_ga(X3, X6, mergesortcE_out_ga(X5, X4)) → U31_ga(X3, X4, mergesortcE_in_gg(X6, []))
U33_ga(X3, X7, mergesortcE_out_ga(X6, .(X8))) → U34_ga(X3, X8, mergesortcE_in_ga(X7))
U21_gaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X2), .(X3), X4)
mergesortcE_in_gg([], []) → mergesortcE_out_gg([], [])
mergesortcE_in_gg(.(.(X3)), X4) → U27_gg(X3, X4, splitcD_in_agaa(.(X3)))
U29_ga(X3, mergesortcE_out_ga(X6, X4)) → mergesortcE_out_ga(.(.(X3)), X4)
U31_ga(X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_ga(.(.(X3)), X4)
U34_ga(X3, X8, mergesortcE_out_ga(X7, .(X9))) → U35_ga(X3, mergecC_in_gga(.(X8), X9))
U27_gg(X3, X4, splitcD_out_agaa(.(X3), X5, X6)) → U28_gg(X3, X4, X6, mergesortcE_in_gg(X5, []))
U27_gg(X3, X4, splitcD_out_agaa(.(X3), X5, X6)) → U30_gg(X3, X4, X6, mergesortcE_in_gg(X5, X4))
U35_ga(X3, mergecC_out_gga(.(X8), X9, X5)) → mergesortcE_out_ga(.(.(X3)), .(X5))
U28_gg(X3, X4, X6, mergesortcE_out_gg(X5, [])) → U29_gg(X3, X4, mergesortcE_in_gg(X6, X4))
U30_gg(X3, X4, X6, mergesortcE_out_gg(X5, X4)) → U31_gg(X3, X4, mergesortcE_in_gg(X6, []))
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X2), .(X3)) → U36_gga(X2, X3, mergecC_in_gga(.(X2), X3))
U29_gg(X3, X4, mergesortcE_out_gg(X6, X4)) → mergesortcE_out_gg(.(.(X3)), X4)
mergesortcE_in_gg(.([]), .([])) → mergesortcE_out_gg(.([]), .([]))
mergesortcE_in_gg(.(.(X3)), .(X5)) → U32_gg(X3, X5, splitcD_in_agaa(.(X3)))
U31_gg(X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_gg(.(.(X3)), X4)
U36_gga(X2, X3, mergecC_out_gga(.(X2), X3, X4)) → mergecC_out_gga(.(X2), .(X3), .(X4))
U32_gg(X3, X5, splitcD_out_agaa(.(X3), X6, X7)) → U33_gg(X3, X5, X7, mergesortcE_in_ga(X6))
U33_gg(X3, X5, X7, mergesortcE_out_ga(X6, .(X8))) → U34_gg(X3, X5, X8, mergesortcE_in_ga(X7))
U34_gg(X3, X5, X8, mergesortcE_out_ga(X7, .(X9))) → U35_gg(X3, X5, mergecC_in_ggg(.(X8), X9, X5))
U35_gg(X3, X5, mergecC_out_ggg(.(X8), X9, X5)) → mergesortcE_out_gg(.(.(X3)), .(X5))
mergecC_in_ggg(X1, [], X1) → mergecC_out_ggg(X1, [], X1)
mergecC_in_ggg(.(X2), .(X3), .(X4)) → U36_ggg(X2, X3, X4, mergecC_in_ggg(.(X2), X3, X4))
U36_ggg(X2, X3, X4, mergecC_out_ggg(.(X2), X3, X4)) → mergecC_out_ggg(.(X2), .(X3), .(X4))

The set Q consists of the following terms:

splitcD_in_agaa(x0)
mergesortcE_in_ga(x0)
U26_agaa(x0, x1)
U27_ga(x0, x1)
U32_ga(x0, x1)
splitcA_in_gaa(x0)
U28_ga(x0, x1, x2)
U30_ga(x0, x1, x2)
U33_ga(x0, x1, x2)
U21_gaa(x0, x1)
mergesortcE_in_gg(x0, x1)
U29_ga(x0, x1)
U31_ga(x0, x1, x2)
U34_ga(x0, x1, x2)
U27_gg(x0, x1, x2)
U35_ga(x0, x1)
U28_gg(x0, x1, x2, x3)
U30_gg(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U29_gg(x0, x1, x2)
U31_gg(x0, x1, x2)
U36_gga(x0, x1, x2)
U32_gg(x0, x1, x2)
U33_gg(x0, x1, x2, x3)
U34_gg(x0, x1, x2, x3)
U35_gg(x0, x1, x2)
mergecC_in_ggg(x0, x1, x2)
U36_ggg(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(30) QDPQMonotonicMRRProof (EQUIVALENT transformation)

By using the Q-monotonic rule removal processor with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented such that it always occurs at a strongly monotonic position in a (P,Q,R)-chain.
Strictly oriented dependency pairs:

U4_GA(X3, splitcD_out_agaa(.(X3), X5, X6)) → MERGESORTE_IN_GA(X5)
U4_GA(X3, splitcD_out_agaa(.(X3), X5, X6)) → U6_GA(X3, X6, mergesortcE_in_ga(X5))


Used ordering: Polynomial interpretation [POLO]:

POL(.(x1)) = 1 + 2·x1   
POL(MERGESORTE_IN_GA(x1)) = 1 + x1   
POL(U21_gaa(x1, x2)) = 1 + 2·x2   
POL(U26_agaa(x1, x2)) = 1 + x1 + x2   
POL(U27_ga(x1, x2)) = 0   
POL(U27_gg(x1, x2, x3)) = 2·x1 + 2·x2   
POL(U28_ga(x1, x2, x3)) = 0   
POL(U28_gg(x1, x2, x3, x4)) = x1   
POL(U29_ga(x1, x2)) = 0   
POL(U29_gg(x1, x2, x3)) = 0   
POL(U30_ga(x1, x2, x3)) = 0   
POL(U30_gg(x1, x2, x3, x4)) = 2·x1 + 2·x2   
POL(U31_ga(x1, x2, x3)) = 0   
POL(U31_gg(x1, x2, x3)) = 2·x1 + x2   
POL(U32_ga(x1, x2)) = 0   
POL(U32_gg(x1, x2, x3)) = 2 + 2·x2   
POL(U33_ga(x1, x2, x3)) = 0   
POL(U33_gg(x1, x2, x3, x4)) = 2 + x2   
POL(U34_ga(x1, x2, x3)) = 0   
POL(U34_gg(x1, x2, x3, x4)) = 2 + x2   
POL(U35_ga(x1, x2)) = 0   
POL(U35_gg(x1, x2, x3)) = 1   
POL(U36_gga(x1, x2, x3)) = 0   
POL(U36_ggg(x1, x2, x3, x4)) = 2   
POL(U4_GA(x1, x2)) = 1 + x2   
POL(U6_GA(x1, x2, x3)) = 1 + x1 + x2   
POL([]) = 0   
POL(mergecC_in_gga(x1, x2)) = 0   
POL(mergecC_in_ggg(x1, x2, x3)) = 2   
POL(mergecC_out_gga(x1, x2, x3)) = 0   
POL(mergecC_out_ggg(x1, x2, x3)) = 0   
POL(mergesortcE_in_ga(x1)) = 1   
POL(mergesortcE_in_gg(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(mergesortcE_out_ga(x1, x2)) = 0   
POL(mergesortcE_out_gg(x1, x2)) = 0   
POL(splitcA_in_gaa(x1)) = x1   
POL(splitcA_out_gaa(x1, x2, x3)) = x2 + 2·x3   
POL(splitcD_in_agaa(x1)) = 2 + 2·x1   
POL(splitcD_out_agaa(x1, x2, x3)) = x1 + x2 + x3   

(31) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U6_GA(X3, X6, mergesortcE_out_ga(X5, X7)) → MERGESORTE_IN_GA(X6)
MERGESORTE_IN_GA(.(.(X3))) → U4_GA(X3, U26_agaa(.(X3), U21_gaa(X3, splitcA_in_gaa(X3))))

The TRS R consists of the following rules:

splitcD_in_agaa(X2) → U26_agaa(X2, splitcA_in_gaa(X2))
mergesortcE_in_ga([]) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.([])) → mergesortcE_out_ga(.([]), .([]))
mergesortcE_in_ga(.(.(X3))) → U27_ga(X3, splitcD_in_agaa(.(X3)))
mergesortcE_in_ga(.(.(X3))) → U32_ga(X3, splitcD_in_agaa(.(X3)))
U26_agaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X2, .(X3), X4)
U27_ga(X3, splitcD_out_agaa(.(X3), X5, X6)) → U28_ga(X3, X6, mergesortcE_in_gg(X5, []))
U27_ga(X3, splitcD_out_agaa(.(X3), X5, X6)) → U30_ga(X3, X6, mergesortcE_in_ga(X5))
U32_ga(X3, splitcD_out_agaa(.(X3), X6, X7)) → U33_ga(X3, X7, mergesortcE_in_ga(X6))
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X2)) → U21_gaa(X2, splitcA_in_gaa(X2))
U28_ga(X3, X6, mergesortcE_out_gg(X5, [])) → U29_ga(X3, mergesortcE_in_ga(X6))
U30_ga(X3, X6, mergesortcE_out_ga(X5, X4)) → U31_ga(X3, X4, mergesortcE_in_gg(X6, []))
U33_ga(X3, X7, mergesortcE_out_ga(X6, .(X8))) → U34_ga(X3, X8, mergesortcE_in_ga(X7))
U21_gaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X2), .(X3), X4)
mergesortcE_in_gg([], []) → mergesortcE_out_gg([], [])
mergesortcE_in_gg(.(.(X3)), X4) → U27_gg(X3, X4, splitcD_in_agaa(.(X3)))
U29_ga(X3, mergesortcE_out_ga(X6, X4)) → mergesortcE_out_ga(.(.(X3)), X4)
U31_ga(X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_ga(.(.(X3)), X4)
U34_ga(X3, X8, mergesortcE_out_ga(X7, .(X9))) → U35_ga(X3, mergecC_in_gga(.(X8), X9))
U27_gg(X3, X4, splitcD_out_agaa(.(X3), X5, X6)) → U28_gg(X3, X4, X6, mergesortcE_in_gg(X5, []))
U27_gg(X3, X4, splitcD_out_agaa(.(X3), X5, X6)) → U30_gg(X3, X4, X6, mergesortcE_in_gg(X5, X4))
U35_ga(X3, mergecC_out_gga(.(X8), X9, X5)) → mergesortcE_out_ga(.(.(X3)), .(X5))
U28_gg(X3, X4, X6, mergesortcE_out_gg(X5, [])) → U29_gg(X3, X4, mergesortcE_in_gg(X6, X4))
U30_gg(X3, X4, X6, mergesortcE_out_gg(X5, X4)) → U31_gg(X3, X4, mergesortcE_in_gg(X6, []))
mergecC_in_gga(X1, []) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X2), .(X3)) → U36_gga(X2, X3, mergecC_in_gga(.(X2), X3))
U29_gg(X3, X4, mergesortcE_out_gg(X6, X4)) → mergesortcE_out_gg(.(.(X3)), X4)
mergesortcE_in_gg(.([]), .([])) → mergesortcE_out_gg(.([]), .([]))
mergesortcE_in_gg(.(.(X3)), .(X5)) → U32_gg(X3, X5, splitcD_in_agaa(.(X3)))
U31_gg(X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_gg(.(.(X3)), X4)
U36_gga(X2, X3, mergecC_out_gga(.(X2), X3, X4)) → mergecC_out_gga(.(X2), .(X3), .(X4))
U32_gg(X3, X5, splitcD_out_agaa(.(X3), X6, X7)) → U33_gg(X3, X5, X7, mergesortcE_in_ga(X6))
U33_gg(X3, X5, X7, mergesortcE_out_ga(X6, .(X8))) → U34_gg(X3, X5, X8, mergesortcE_in_ga(X7))
U34_gg(X3, X5, X8, mergesortcE_out_ga(X7, .(X9))) → U35_gg(X3, X5, mergecC_in_ggg(.(X8), X9, X5))
U35_gg(X3, X5, mergecC_out_ggg(.(X8), X9, X5)) → mergesortcE_out_gg(.(.(X3)), .(X5))
mergecC_in_ggg(X1, [], X1) → mergecC_out_ggg(X1, [], X1)
mergecC_in_ggg(.(X2), .(X3), .(X4)) → U36_ggg(X2, X3, X4, mergecC_in_ggg(.(X2), X3, X4))
U36_ggg(X2, X3, X4, mergecC_out_ggg(.(X2), X3, X4)) → mergecC_out_ggg(.(X2), .(X3), .(X4))

The set Q consists of the following terms:

splitcD_in_agaa(x0)
mergesortcE_in_ga(x0)
U26_agaa(x0, x1)
U27_ga(x0, x1)
U32_ga(x0, x1)
splitcA_in_gaa(x0)
U28_ga(x0, x1, x2)
U30_ga(x0, x1, x2)
U33_ga(x0, x1, x2)
U21_gaa(x0, x1)
mergesortcE_in_gg(x0, x1)
U29_ga(x0, x1)
U31_ga(x0, x1, x2)
U34_ga(x0, x1, x2)
U27_gg(x0, x1, x2)
U35_ga(x0, x1)
U28_gg(x0, x1, x2, x3)
U30_gg(x0, x1, x2, x3)
mergecC_in_gga(x0, x1)
U29_gg(x0, x1, x2)
U31_gg(x0, x1, x2)
U36_gga(x0, x1, x2)
U32_gg(x0, x1, x2)
U33_gg(x0, x1, x2, x3)
U34_gg(x0, x1, x2, x3)
U35_gg(x0, x1, x2)
mergecC_in_ggg(x0, x1, x2)
U36_ggg(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(32) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(33) TRUE

(34) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U14_GA(X1, X2, X3, X4, splitcD_in_agaa(X2, X3, X5, X6))
U14_GA(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)

The TRS R consists of the following rules:

splitcD_in_agaa(X1, X2, .(X1, X3), X4) → U26_agaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U21_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U21_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)
U26_agaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X1, X2, .(X1, X3), X4)
mergesortcB_in_ga([], []) → mergesortcB_out_ga([], [])
mergesortcB_in_ga(.(X1, []), .(X1, [])) → mergesortcB_out_ga(.(X1, []), .(X1, []))
mergesortcB_in_ga(.(X1, .(X2, X3)), X4) → U22_ga(X1, X2, X3, X4, splitcD_in_agaa(X2, X3, X5, X6))
U22_ga(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_in_ga(.(X1, X6), X7))
U23_ga(X1, X2, X3, X4, X5, X6, mergesortcB_out_ga(.(X1, X6), X7)) → U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X5, X8))
mergesortcE_in_ga([], []) → mergesortcE_out_ga([], [])
mergesortcE_in_ga(.(X1, []), .(X1, [])) → mergesortcE_out_ga(.(X1, []), .(X1, []))
mergesortcE_in_ga(.(X1, .(X2, X3)), X4) → U27_ga(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg([], []) → mergesortcE_out_gg([], [])
mergesortcE_in_gg(.(X1, []), .(X1, [])) → mergesortcE_out_gg(.(X1, []), .(X1, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), X4) → U27_gg(X1, X2, X3, X4, splitcD_in_agaa(X1, .(X2, X3), X5, X6))
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, []))
mergesortcE_in_gg(.(X1, .(X2, X3)), .(X4, X5)) → U32_gg(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_gg(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
mergesortcE_in_ga(.(X1, .(X2, X3)), .(X4, X5)) → U32_ga(X1, X2, X3, X4, X5, splitcD_in_agaa(X1, .(X2, X3), X6, X7))
U32_ga(X1, X2, X3, X4, X5, splitcD_out_agaa(X1, .(X2, X3), X6, X7)) → U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_in_ga(X6, .(X4, X8)))
U33_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_ga(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_ga(X1, X2, X3, X4, X5, mergecC_in_gga(.(X4, X8), X9, X5))
mergecC_in_gga([], X1, X1) → mergecC_out_gga([], X1, X1)
mergecC_in_gga(X1, [], X1) → mergecC_out_gga(X1, [], X1)
mergecC_in_gga(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_gga(X1, X2, X3, X4, mergecC_in_gga(.(X1, X2), X3, X4))
U36_gga(X1, X2, X3, X4, mergecC_out_gga(.(X1, X2), X3, X4)) → mergecC_out_gga(.(X1, X2), .(X1, X3), .(X1, X4))
U35_ga(X1, X2, X3, X4, X5, mergecC_out_gga(.(X4, X8), X9, X5)) → mergesortcE_out_ga(.(X1, .(X2, X3)), .(X4, X5))
U33_gg(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X6, .(X4, X8))) → U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_in_ga(X7, .(X4, X9)))
U34_gg(X1, X2, X3, X4, X5, X6, X7, X8, mergesortcE_out_ga(X7, .(X4, X9))) → U35_gg(X1, X2, X3, X4, X5, mergecC_in_ggg(.(X4, X8), X9, X5))
mergecC_in_ggg([], X1, X1) → mergecC_out_ggg([], X1, X1)
mergecC_in_ggg(X1, [], X1) → mergecC_out_ggg(X1, [], X1)
mergecC_in_ggg(.(X1, X2), .(X1, X3), .(X1, X4)) → U36_ggg(X1, X2, X3, X4, mergecC_in_ggg(.(X1, X2), X3, X4))
U36_ggg(X1, X2, X3, X4, mergecC_out_ggg(.(X1, X2), X3, X4)) → mergecC_out_ggg(.(X1, X2), .(X1, X3), .(X1, X4))
U35_gg(X1, X2, X3, X4, X5, mergecC_out_ggg(.(X4, X8), X9, X5)) → mergesortcE_out_gg(.(X1, .(X2, X3)), .(X4, X5))
U28_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, X4))
U29_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, X4)) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U27_gg(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_in_gg(X5, X4))
U30_gg(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, X4)) → U31_gg(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_gg(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_gg(.(X1, .(X2, X3)), X4)
U28_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_gg(X5, [])) → U29_ga(X1, X2, X3, X4, mergesortcE_in_ga(X6, X4))
U29_ga(X1, X2, X3, X4, mergesortcE_out_ga(X6, X4)) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U27_ga(X1, X2, X3, X4, splitcD_out_agaa(X1, .(X2, X3), X5, X6)) → U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_in_ga(X5, X4))
U30_ga(X1, X2, X3, X4, X5, X6, mergesortcE_out_ga(X5, X4)) → U31_ga(X1, X2, X3, X4, mergesortcE_in_gg(X6, []))
U31_ga(X1, X2, X3, X4, mergesortcE_out_gg(X6, [])) → mergesortcE_out_ga(.(X1, .(X2, X3)), X4)
U24_ga(X1, X2, X3, X4, X5, X6, X7, mergesortcE_out_ga(X5, X8)) → U25_ga(X1, X2, X3, X4, mergecC_in_gga(X7, X8, X4))
U25_ga(X1, X2, X3, X4, mergecC_out_gga(X7, X8, X4)) → mergesortcB_out_ga(.(X1, .(X2, X3)), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U21_gaa(x1, x2, x3, x4, x5)  =  U21_gaa(x2, x5)
mergesortcB_in_ga(x1, x2)  =  mergesortcB_in_ga(x1)
mergesortcB_out_ga(x1, x2)  =  mergesortcB_out_ga(x1, x2)
U22_ga(x1, x2, x3, x4, x5)  =  U22_ga(x3, x5)
U23_ga(x1, x2, x3, x4, x5, x6, x7)  =  U23_ga(x3, x5, x7)
U24_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U24_ga(x3, x7, x8)
mergesortcE_in_ga(x1, x2)  =  mergesortcE_in_ga(x1)
mergesortcE_out_ga(x1, x2)  =  mergesortcE_out_ga(x1, x2)
U27_ga(x1, x2, x3, x4, x5)  =  U27_ga(x3, x5)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x3, x6, x7)
mergesortcE_in_gg(x1, x2)  =  mergesortcE_in_gg(x1, x2)
mergesortcE_out_gg(x1, x2)  =  mergesortcE_out_gg(x1, x2)
U27_gg(x1, x2, x3, x4, x5)  =  U27_gg(x3, x4, x5)
U28_gg(x1, x2, x3, x4, x5, x6, x7)  =  U28_gg(x3, x4, x6, x7)
U32_gg(x1, x2, x3, x4, x5, x6)  =  U32_gg(x3, x5, x6)
U33_gg(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_gg(x3, x5, x7, x8)
U32_ga(x1, x2, x3, x4, x5, x6)  =  U32_ga(x3, x6)
U33_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U33_ga(x3, x7, x8)
splitcD_in_agaa(x1, x2, x3, x4)  =  splitcD_in_agaa(x2)
U26_agaa(x1, x2, x3, x4, x5)  =  U26_agaa(x2, x5)
splitcD_out_agaa(x1, x2, x3, x4)  =  splitcD_out_agaa(x2, x3, x4)
U34_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_ga(x3, x8, x9)
U35_ga(x1, x2, x3, x4, x5, x6)  =  U35_ga(x3, x6)
mergecC_in_gga(x1, x2, x3)  =  mergecC_in_gga(x1, x2)
mergecC_out_gga(x1, x2, x3)  =  mergecC_out_gga(x1, x2, x3)
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x2, x3, x5)
U34_gg(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_gg(x3, x5, x8, x9)
U35_gg(x1, x2, x3, x4, x5, x6)  =  U35_gg(x3, x5, x6)
mergecC_in_ggg(x1, x2, x3)  =  mergecC_in_ggg(x1, x2, x3)
mergecC_out_ggg(x1, x2, x3)  =  mergecC_out_ggg(x1, x2, x3)
U36_ggg(x1, x2, x3, x4, x5)  =  U36_ggg(x2, x3, x4, x5)
U29_gg(x1, x2, x3, x4, x5)  =  U29_gg(x3, x4, x5)
U30_gg(x1, x2, x3, x4, x5, x6, x7)  =  U30_gg(x3, x4, x6, x7)
U31_gg(x1, x2, x3, x4, x5)  =  U31_gg(x3, x4, x5)
U29_ga(x1, x2, x3, x4, x5)  =  U29_ga(x3, x5)
U30_ga(x1, x2, x3, x4, x5, x6, x7)  =  U30_ga(x3, x6, x7)
U31_ga(x1, x2, x3, x4, x5)  =  U31_ga(x3, x4, x5)
U25_ga(x1, x2, x3, x4, x5)  =  U25_ga(x3, x5)
MERGESORTB_IN_GA(x1, x2)  =  MERGESORTB_IN_GA(x1)
U14_GA(x1, x2, x3, x4, x5)  =  U14_GA(x3, x5)

We have to consider all (P,R,Pi)-chains

(35) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(36) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GA(.(X1, .(X2, X3)), X4) → U14_GA(X1, X2, X3, X4, splitcD_in_agaa(X2, X3, X5, X6))
U14_GA(X1, X2, X3, X4, splitcD_out_agaa(X2, X3, X5, X6)) → MERGESORTB_IN_GA(.(X1, X6), X7)

The TRS R consists of the following rules:

splitcD_in_agaa(X1, X2, .(X1, X3), X4) → U26_agaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U26_agaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X1, X2, .(X1, X3), X4)
splitcA_in_gaa([], [], []) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X1, X2), .(X1, X3), X4) → U21_gaa(X1, X2, X3, X4, splitcA_in_gaa(X2, X4, X3))
U21_gaa(X1, X2, X3, X4, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X1, X2), .(X1, X3), X4)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
splitcA_in_gaa(x1, x2, x3)  =  splitcA_in_gaa(x1)
[]  =  []
splitcA_out_gaa(x1, x2, x3)  =  splitcA_out_gaa(x1, x2, x3)
U21_gaa(x1, x2, x3, x4, x5)  =  U21_gaa(x2, x5)
splitcD_in_agaa(x1, x2, x3, x4)  =  splitcD_in_agaa(x2)
U26_agaa(x1, x2, x3, x4, x5)  =  U26_agaa(x2, x5)
splitcD_out_agaa(x1, x2, x3, x4)  =  splitcD_out_agaa(x2, x3, x4)
MERGESORTB_IN_GA(x1, x2)  =  MERGESORTB_IN_GA(x1)
U14_GA(x1, x2, x3, x4, x5)  =  U14_GA(x3, x5)

We have to consider all (P,R,Pi)-chains

(37) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(38) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GA(.(.(X3))) → U14_GA(X3, splitcD_in_agaa(X3))
U14_GA(X3, splitcD_out_agaa(X3, X5, X6)) → MERGESORTB_IN_GA(.(X6))

The TRS R consists of the following rules:

splitcD_in_agaa(X2) → U26_agaa(X2, splitcA_in_gaa(X2))
U26_agaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X2, .(X3), X4)
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X2)) → U21_gaa(X2, splitcA_in_gaa(X2))
U21_gaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X2), .(X3), X4)

The set Q consists of the following terms:

splitcD_in_agaa(x0)
U26_agaa(x0, x1)
splitcA_in_gaa(x0)
U21_gaa(x0, x1)

We have to consider all (P,Q,R)-chains.

(39) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule MERGESORTB_IN_GA(.(.(X3))) → U14_GA(X3, splitcD_in_agaa(X3)) at position [1] we obtained the following new rules [LPAR04]:

MERGESORTB_IN_GA(.(.(X3))) → U14_GA(X3, U26_agaa(X3, splitcA_in_gaa(X3)))

(40) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U14_GA(X3, splitcD_out_agaa(X3, X5, X6)) → MERGESORTB_IN_GA(.(X6))
MERGESORTB_IN_GA(.(.(X3))) → U14_GA(X3, U26_agaa(X3, splitcA_in_gaa(X3)))

The TRS R consists of the following rules:

splitcD_in_agaa(X2) → U26_agaa(X2, splitcA_in_gaa(X2))
U26_agaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X2, .(X3), X4)
splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X2)) → U21_gaa(X2, splitcA_in_gaa(X2))
U21_gaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X2), .(X3), X4)

The set Q consists of the following terms:

splitcD_in_agaa(x0)
U26_agaa(x0, x1)
splitcA_in_gaa(x0)
U21_gaa(x0, x1)

We have to consider all (P,Q,R)-chains.

(41) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(42) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U14_GA(X3, splitcD_out_agaa(X3, X5, X6)) → MERGESORTB_IN_GA(.(X6))
MERGESORTB_IN_GA(.(.(X3))) → U14_GA(X3, U26_agaa(X3, splitcA_in_gaa(X3)))

The TRS R consists of the following rules:

splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X2)) → U21_gaa(X2, splitcA_in_gaa(X2))
U26_agaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X2, .(X3), X4)
U21_gaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X2), .(X3), X4)

The set Q consists of the following terms:

splitcD_in_agaa(x0)
U26_agaa(x0, x1)
splitcA_in_gaa(x0)
U21_gaa(x0, x1)

We have to consider all (P,Q,R)-chains.

(43) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

splitcD_in_agaa(x0)

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U14_GA(X3, splitcD_out_agaa(X3, X5, X6)) → MERGESORTB_IN_GA(.(X6))
MERGESORTB_IN_GA(.(.(X3))) → U14_GA(X3, U26_agaa(X3, splitcA_in_gaa(X3)))

The TRS R consists of the following rules:

splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X2)) → U21_gaa(X2, splitcA_in_gaa(X2))
U26_agaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X2, .(X3), X4)
U21_gaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X2), .(X3), X4)

The set Q consists of the following terms:

U26_agaa(x0, x1)
splitcA_in_gaa(x0)
U21_gaa(x0, x1)

We have to consider all (P,Q,R)-chains.

(45) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


U14_GA(X3, splitcD_out_agaa(X3, X5, X6)) → MERGESORTB_IN_GA(.(X6))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1)) = 1 + x1   
POL(MERGESORTB_IN_GA(x1)) = x1   
POL(U14_GA(x1, x2)) = 1 + x2   
POL(U21_gaa(x1, x2)) = 1 + x2   
POL(U26_agaa(x1, x2)) = 1 + x2   
POL([]) = 0   
POL(splitcA_in_gaa(x1)) = x1   
POL(splitcA_out_gaa(x1, x2, x3)) = x2 + x3   
POL(splitcD_out_agaa(x1, x2, x3)) = 1 + x3   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X2)) → U21_gaa(X2, splitcA_in_gaa(X2))
U26_agaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X2, .(X3), X4)
U21_gaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X2), .(X3), X4)

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MERGESORTB_IN_GA(.(.(X3))) → U14_GA(X3, U26_agaa(X3, splitcA_in_gaa(X3)))

The TRS R consists of the following rules:

splitcA_in_gaa([]) → splitcA_out_gaa([], [], [])
splitcA_in_gaa(.(X2)) → U21_gaa(X2, splitcA_in_gaa(X2))
U26_agaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcD_out_agaa(X2, .(X3), X4)
U21_gaa(X2, splitcA_out_gaa(X2, X4, X3)) → splitcA_out_gaa(.(X2), .(X3), X4)

The set Q consists of the following terms:

U26_agaa(x0, x1)
splitcA_in_gaa(x0)
U21_gaa(x0, x1)

We have to consider all (P,Q,R)-chains.

(47) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(48) TRUE